Type Theory
-----------

<!--
SPDX-FileCopyrightText: Chris Pressey, the original author of this work, has dedicated it to the public domain.

SPDX-License-Identifier: CC0-1.0
-->

[(Up)](../../README.md#topics) | _See also: [Type Systems](../Type%20Systems/README.md#type-systems)_

- - - -

Works regarding the formal study of types, primarily in its original meaning as a means to avoid paradoxes in logic, and secondarily as it is studied in the modern world to provide a theoretical basis for type systems in programming languages.

### Web resources

[Type Theory (Stanford Encyclopedia of Philosophy)](https://plato.stanford.edu/entries/type-theory/) ★★ [💭](commentary/cpressey.md#type-theory-stanford-encyclopedia-of-philosophy)

[Intuitionistic Type Theory (Stanford Encyclopedia of Philosophy)](https://plato.stanford.edu/entries/type-theory-intuitionistic/) ★★ [💭](commentary/cpressey.md#intuitionistic-type-theory-stanford-encyclopedia-of-philosophy)

[Does there exist a Turing complete typed lambda calculus?](https://cs.stackexchange.com/questions/2638/does-there-exist-a-turing-complete-typed-lambda-calculus) ★

[Characterization of lambda-terms that have union types](https://cs.stackexchange.com/questions/62/characterization-of-lambda-terms-that-have-union-types/88#88) ★

[Type Theory and Mathematical Logic \| artagnon.com](https://artagnon.com/logic) ★

[Typed Combinators](http://chriswarbo.net/blog/2012-12-01-typed_combinators.html) ★

[Recursive Types for Free! (Philip Wadler)](https://homepages.inf.ed.ac.uk/wadler/papers/free-rectypes/free-rectypes.txt) ★

[Computational type theory - Scholarpedia](http://www.scholarpedia.org/article/Computational_type_theory)

_(in [Type Systems](../Type%20Systems/README.md#type-systems))_ [The algebra (and calculus!) of algebraic data types](https://codewords.recurse.com/issues/three/algebra-and-calculus-of-algebraic-data-types) ★★★


### Papers

Recursive Types (online @ [www.ps.uni-saarland.de](https://www.ps.uni-saarland.de/courses/seminar-ws02/RecursiveTypes.pdf)) ★ [💭](commentary/cpressey.md#recursive-types)

On Universes in Type Theory (online @ [www2.math.uu.se](https://www2.math.uu.se/~palmgren/universe.pdf), [media.githubusercontent.com](https://media.githubusercontent.com/media/storagelfs/books/main/Theorethical%20Computer%20Science/Dependent%20Type%20Theory/Palmgren.%20On%20Universes%20in%20Type%20Theory.%201998.pdf)) ★ [💭](commentary/cpressey.md#on-universes-in-type-theory)

The Gentle Art of Levitation (online @ [personal.cis.strath.ac.uk](https://personal.cis.strath.ac.uk/conor.mcbride/levitation.pdf)) ★ [💭](commentary/cpressey.md#the-gentle-art-of-levitation)

Breaking Through the Normalization Barrier: A Self-Interpreter for F-omega (online @ [web.cs.ucla.edu](https://web.cs.ucla.edu/~palsberg/paper/popl16-full.pdf))

A lean specification for GADTs: system F with first-class equality proofs (online @ [link.springer.com](https://link.springer.com/article/10.1007/s10990-011-9065-0)) ★ [💭](commentary/cpressey.md#a-lean-specification-for-gadts-system-f-with-first-class-equality-proofs)

Observational Equality, Now! (online @ [strictlypositive.org](http://strictlypositive.org/obseqnow.pdf)) [💭](commentary/cpressey.md#observational-equality-now)

_(in [Calculus of Constructions](../Calculus%20of%20Constructions/README.md#calculus-of-constructions))_ [The Calculus of Inductive Constructions](https://www.cs.uoregon.edu/research/summerschool/summer11/lectures/oplss-herbelin1.pdf) ★ [💭](commentary/cpressey.md#the-calculus-of-inductive-constructions)

_(in [Computational Complexity](../Computational%20Complexity/README.md#computational-complexity))_ The Typed Lambda Calculus is not Elementary Recursive (online @ [www.cs.cornell.edu](https://www.cs.cornell.edu/courses/cs6110/2012sp/Statman-typed-lambda-calculus.pdf)) ★

_(in [Name Binding](../Name%20Binding/README.md#name-binding))_ [A Type and Scope Safe Universe of Syntaxes with Binding](https://pure.strath.ac.uk/ws/portalfiles/portal/114903157/Allais_etal_ICFP2018_A_type_and_scope_safe_universe_of_syntaxes_with_binding.pdf)

_(in [Type Systems](../Type%20Systems/README.md#type-systems))_ Abstract Types have Existential Type (online @ [homepages.inf.ed.ac.uk](https://homepages.inf.ed.ac.uk/gdp/publications/Abstract_existential.pdf)) 🏛️


### Books

Basic Simple Type Theory (borrow with print disabilities @ [archive.org](https://archive.org/details/basicsimpletypet0000hind)) ★ [💭](commentary/cpressey.md#basic-simple-type-theory)

Type Theory and Functional Programming (online @ [www.cs.kent.ac.uk](https://www.cs.kent.ac.uk/people/staff/sjt/TTFP/ttfp.pdf))

Programming in Martin-Löf’s Type Theory (online @ [www.cse.chalmers.se](http://www.cse.chalmers.se/research/group/logic/book/))